(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun u () Real)
(assert (not (exists ((s Real)) (=> (and (= i 0.0 (+ q (/ a a)) 0.0 0.0) (<= a (- 2.0 d (- u)))) (= (<= s 0.0) (<= 0.0 i (* d (- u))))))))
(assert (exists ((t Real)) (and (<= (* (/ 2.0 0.0 0.0) j) k) (= (- b e) 1.0))))
(assert (= b (+ e p) 0.0 (+ u p) 0.0 (/ i 0.0)))
(check-sat)
